|
|
Hardware Accelerated Functional Verification
Zachariášová, Marcela ; Kotásek, Zdeněk (oponent) ; Kajan, Michal (vedoucí práce)
Functional verification is a widespread technique to check whether a hardware system satisfies a given correctness specification. The complexity of modern computer systems is rapidly rising and the verification process takes a significant amount of time. It is a challenging task to find appropriate acceleration techniques for this process. In this thesis, we describe theoretical principles of different verification approaches such as simulation and testing, functional verification, and formal analysis and verification. In particular, we focus on creating verification environments in the SystemVerilog language. The analysis part describes the requirements on a system for acceleration of functional verification, the most important being the option to easily enable acceleration and time equivalence of an accelerated and a non-accelerated run of a verification. The thesis further introduces a design of a verification framework that exploits the field-programmable gate array technology, while retaining the possibility to run verification in the user-friendly debugging environment of a simulator. According to the experiments carried out on a prototype implementation, the achieved acceleration is proportional to the number of checked transactions and the complexity of the verified system. The maximum acceleration achieved on the set of experiments was over 130 times.
|
|
|
Prostředí pro funkční verifikaci multi-sběrnic podle UVM standardu
Beneš, Tomáš ; Šišmiš, Lukáš (oponent) ; Kekely, Lukáš (vedoucí práce)
Práce se zabývá návrhem a následnou implementací prostředí pro verifikace multi-sběrnic s využitím principů univerzální verifikační metodologie (UVM). Dále se zabývá implementací verifikací tří FPGA konkrétních komponent využívající multi-sběrnice jako vstupní a výstupní rozhraní. Implementace prostředí i všech verifikací je napsaná v jazyce SystemVerilog s využitím knihovny implementující základní konstrukce pro UVM. Dosažené výsledky práce jsou funkční a jednoduše znovupoužitelné při tvorbě dalších verifikací využívající multi-sběrnic. Navržené prostředí se dají využít jako struktura pro tvorbu dalších verifikačních prostředí pro jiné sběrnice.
|
|
|
Specifikace scénářů portovatelných stimulů pro moduly procesoru RISC-V
Bardonek, Petr ; Bidlo, Michal (oponent) ; Zachariášová, Marcela (vedoucí práce)
Práce se zabývá návrhem a implementací verifikačních scénářů portovatelných stimulů pro vybrané moduly procesoru Berkelium implementujícím architekturu RISC-V od společnosti Codasip. Cílem této práce je s využitím nového standardu pro Portable Stimulus připravovaného organizací Accellera navrhnout a implementovat scénáře portovatelných stimulů za použití nástroje Questa InFact od společnosti Mentor. Takto navržené scénáře portovatelných stimulů se připojí k již existujícím verifikačním prostředím vytvořených podle metodiky UVM a následně se pomocí nich provede verifikace modulů procesoru Berkelium implementujícím architekturu RISC-V. Poslední částí práce je vyhodnocení úrovně portovatelnosti implementovaných scénářů do jednotlivých úrovní procesoru Berkelium implementujícím architekturu RISC-V (IP bloky, subsystémy, systémy jako celek), kdy je snahou využít navržené scénáře napříč všemi verifikovanými úrovněmi.
|
|
|
Funkční verifikace výpočetních jednotek procesoru
Valach, Lukáš ; Lengál, Ondřej (oponent) ; Masařík, Karel (vedoucí práce)
Práce se zaobírá začleněním procesu funkční verifikace do vývojového cyklu návrhu funkčních jednotek v prostředí pro souběžný návrh hardwaru a softwaru systému Codasip. Cílem bylo navrhnout a implementovat verifikační prostředí v jazyku SystemVerilog pro verifikaci automaticky generované hardwarové reprezentace těchto jednotek. Na začátku jsou rozebrány přínosy a obvyklé postupy při funkční verifikaci a vlastnosti systému Codasip. Dále je v práci popsán návrh, implementace, analýza průběhu a výsledků testů verifikace simulačního modelu aritmeticko-logické jednotky. Závěrem jsou zhodnoceny dosažené výsledky práce a navrhnuta zlepšení pro možný další rozvoj verifikačního prostředí.
|
|
|
Zpětnovazební funkční verifikace hardware
Santa, Marek ; Kajan, Michal (oponent) ; Kořenek, Jan (vedoucí práce)
Vyhnout se chybám při vývoji číslicových systémů je téměř nemožné. Přitom brzké odhalení chyb pomáha šetřit čas i peníze. Tato práce se zabývá automatizací zpětné vazby ve funkčních verifikacích různých komponent na spracování dat. Automatická zpětná vazba má za úkol přinést nejen zkrácení času potřebného k ověření funkčnosti systému, ale zejména zlepšit prohledávání okrajových podmínek a zvýšit tak důvěru ve verifikovaný systém. V práci jsou diskutovány principy a postupy jak funkční tak i formální verifikace, metriky poskytující představu o tom, jaká část funkcionality byla pokryta, jsou popsány nedostatky zmíněných technik a identifikován prostor pro zlepšení současného stavu. Následně je představen návrh spětnovazebního verifikačního prostředí využívajícího genetický algoritmus. Na závěr práce jsou shrnuty dosažené výsledky verifikace.
|
|
|
Generátor změn obrazu burzy
Cienciala, Ondřej ; Zachariášová, Marcela (oponent) ; Dvořák, Milan (vedoucí práce)
Tento dokument analyzuje zprávy zasílané burzami NYSE Arca a ISE a popisuje návrh generátoru, který generuje zprávy měnící obraz burzy. Lze ho využít pro testování programů, které pracují s informacemi zasílanými elektronickými burzami. Jsou popsány techniky verifikace řízené pokrytím a generování náhodných vstupních vektorů. Generování zpráv je založeno na XML šabloně, díky čemuž může být generátor použit pro různé burzy.
|
|
| |
|
|
Hardwarově akcelerovaná funkční verifikace procesoru
Funiak, Martin ; Kajan, Michal (oponent) ; Zachariášová, Marcela (vedoucí práce)
Mezi aktuálně používané verifikační přístupy patří funkční verifikace. Při funkční verifikaci se ověřuje korektnost implementace počítačového systému vzhledem k specifikaci. Slabým místem v rámci přístupu funkční verifikace je její časová náročnost, na kterou má vliv pomalá softwarová simulace implicitně paralelních hardwarových systémů. V této práci je představeno řešení využívající hardwarovou akceleraci funkční verifikace procesoru. Úvodní kapitoly tvoří teoretický základ pro následující kapitoly, ve kterých se nachází analýza a výběr řešení, návrh verifikačního prostředí a implementační detaily. Závěr práce obsahuje testování výsledného produktu, zhodnocení výsledků práce a vyhlídky do budoucna.
|
|
|
Funkční verifikace robotického systému pomocí UVM
Krajčír, Stanislav ; Čekan, Ondřej (oponent) ; Zachariášová, Marcela (vedoucí práce)
Jedním z aktuálně nejvíce využívaných přístupů pro verifikaci hardwarových systémů je funkční verifikace. Tato diplomová práce se zabývá tvorbou verifikačního prostředí s využitím metodiky UVM (Universal Verification Methodology) pro ověření korektnosti řídicí jednotky robotického systému s cílem odstranění funkčních chyb z její implementace. Teoretická část práce popisuje základní informace z oblasti funkční verifikace, metody tvorby verifikačního prostředí, jazyk SystemVerilog a problematiku zajištění odolnosti systémů proti poruchám. Následující část práce se zaměřuje na návrh verifikačního prostředí, jeho implementaci a na tvorbu testů sloužících k ověření korektnosti řídicí jednotky. V závěru práce jsou diskutovány a zhodnoceny dosažené výsledky verifikace.
|
|
|
Integrace formálních technik do procesu verifikace procesoru RISC-V
Horký, Jakub ; Šnobl, Pavel (oponent) ; Hruška, Tomáš (vedoucí práce)
Tato práce krátce rozebírá architekturu RISC-V a návrh procesorů a jak jednoduše může vzniknout chyba při jejich vytváření. Dále popisuji, jakým způsobem se snaží funkční verifikace tyto chyby odhalit a jaké jsou její výhody a nedostatky. Konkrétněji se zaměřím, jak vypadá verifikační prostředí podle UVM. Popisuji, jakým způsobem do funkční verifikace zapadá formální verifikace a jaké jsou dostupné nástroje pro formální verifikaci. Ke konci této práce popisuji konkrétně způsob mého postupu při psaní tvrzení (psaných v SVA jazyce) pro RISC-V procesor za použití nástroje pro formální verifikaci tvrzení. Při využití těchto tvrzení pro ověření procesoru v pozdější fázi vývoje, kdy funkční verifikace již měla možnost většinu chyb odhalit, se mi přesto podařilo několik chyb najít.
|
host ::
RSS.